Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Embed ARM ASL specs within OCaml #92

Merged
merged 4 commits into from
Jun 24, 2024
Merged

Embed ARM ASL specs within OCaml #92

merged 4 commits into from
Jun 24, 2024

Conversation

katrinafyi
Copy link
Member

@katrinafyi katrinafyi commented Jun 20, 2024

This is instead of installing the ASL files to disk. This should make the installation less liable to random breakages when installed or linked in an unexpected way.

The binary size increases by 6MB.

@katrinafyi katrinafyi mentioned this pull request Jun 20, 2024
7 tasks
@katrinafyi katrinafyi marked this pull request as draft June 20, 2024 06:25
@katrinafyi katrinafyi changed the title [WIP] Embed ARM ASL specs within OCaml Embed ARM ASL specs within OCaml Jun 21, 2024
@katrinafyi katrinafyi marked this pull request as ready for review June 21, 2024 08:48
katrinafyi added a commit to katrinafyi/pac-nix that referenced this pull request Jun 21, 2024
@katrinafyi katrinafyi changed the base branch from partial_eval to js-of-ocaml June 24, 2024 01:02
@katrinafyi katrinafyi force-pushed the embed-asl-files branch 3 times, most recently from ee70868 to 0b20c65 Compare June 24, 2024 01:33
This is instead of installing the ASL files to disk.
This should make the installation less liable to random
breakages when installed or linked in an unexpected way.

The binary size increases by 6MB.

Updates tests/coverage/run.sh to substitute away the
new file paths of the embedded files, so no coverage
re-generation needed.
this is more useful once the MRA files are bundled.
@katrinafyi katrinafyi merged commit 236460b into js-of-ocaml Jun 24, 2024
2 checks passed
katrinafyi added a commit that referenced this pull request Jun 24, 2024
* extract arm environment into separate file.

* allow loading files from either disk or memory

* use ppx_blob to embed ASL files instead of dune-site

This is instead of installing the ASL files to disk.
This should make the installation less liable to random
breakages when installed or linked in an unexpected way.

The binary size increases by 6MB.

Updates tests/coverage/run.sh to substitute away the
new file paths of the embedded files, so no coverage
re-generation needed.

* replace --aarch64-dir with --export-aarch64

this is more useful once the MRA files are bundled.
@katrinafyi katrinafyi deleted the embed-asl-files branch June 26, 2024 03:42
katrinafyi added a commit that referenced this pull request Jul 1, 2024
* extract arm environment into separate file.

* allow loading files from either disk or memory

* use ppx_blob to embed ASL files instead of dune-site

This is instead of installing the ASL files to disk.
This should make the installation less liable to random
breakages when installed or linked in an unexpected way.

The binary size increases by 6MB.

Updates tests/coverage/run.sh to substitute away the
new file paths of the embedded files, so no coverage
re-generation needed.

* replace --aarch64-dir with --export-aarch64

this is more useful once the MRA files are bundled.
katrinafyi added a commit that referenced this pull request Jul 1, 2024
* Split libASL and isolate Z3 into virtual library (#91)

Z3 links to a native shared library, and so is unsuitable for use via js-of-ocaml. This separates the one use of Z3 in the code (the type-checker's constraint solver) into a separate library which may be stubbed for non-native platforms.

This separates libASL into two parts: libASL_ast which is the minimum needed to define the ASL syntax tree, and libASL which contains the rest of the library. libASL should still be used as the public interface of the library. Since libASL re-exports all of libASL_ast, this should not affect the API visible by downstream users.

This is required since we need to insert a platform-specific library, libASL_support, which introduces z3 only on native builds. The dependency tree now looks like: libASL_ast <- libASL_support (virtual) <- libASL.

* remove pcre library, use ocaml str instead (#93)

PCRE relies on a shared library, precluding its use in Javascript.
instead, we use the standard ocaml "str" library. note, however,
that this supports a smaller subscript of regex (notably no negative
lookahead), and has a different syntax.

see: https://ocaml.org/manual/5.2/api/Str.html

* Embed ARM ASL specs within OCaml (#92)

* extract arm environment into separate file.

* allow loading files from either disk or memory

* use ppx_blob to embed ASL files instead of dune-site

This is instead of installing the ASL files to disk.
This should make the installation less liable to random
breakages when installed or linked in an unexpected way.

The binary size increases by 6MB.

Updates tests/coverage/run.sh to substitute away the
new file paths of the embedded files, so no coverage
re-generation needed.

* replace --aarch64-dir with --export-aarch64

this is more useful once the MRA files are bundled.

* initialising jsoo

* tcheck: make global env0 mutable

necessary for correct unmarshalling, as this
must contain global variables

* dummy libASL to reduce conflicts

* rename libASL parts to stage0/stage1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant